<html>
<head><meta charset="utf-8"><title>Modeling Transmutability · project-safe-transmute · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/index.html">project-safe-transmute</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html">Modeling Transmutability</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="209203744"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/209203744" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#209203744">(Sep 06 2020 at 01:38)</a>:</h4>
<p>I'd like to model out the transmutability rules of the RFC. I've already done this with Typic, but type-level programming isn't exactly a great way to communicate a spec.</p>



<a name="209204053"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/209204053" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#209204053">(Sep 06 2020 at 01:48)</a>:</h4>
<p>I'm currently poking around with <a href="https://docs.racket-lang.org/redex/">Redex</a>. It makes trivial things which are useful for modeling, like flattening products-of-sums into sums-of-products:</p>
<div class="codehilite"><pre><span></span><code><span class="kn">#lang </span><span class="nn">racket</span>

<span class="p">(</span><span class="k">require</span> <span class="n">redex</span><span class="p">)</span>

<span class="p">(</span><span class="n">define-language</span>
  <span class="n">Type</span>

  <span class="p">(</span><span class="n">t</span> <span class="n">::=</span>
     <span class="p">(</span><span class="nb">+</span> <span class="n">t</span> <span class="k">...</span><span class="p">)</span> <span class="c1">; enums</span>
     <span class="p">(</span><span class="n">×</span> <span class="n">t</span> <span class="k">...</span><span class="p">)</span> <span class="c1">; structs</span>
     <span class="n">variable</span><span class="p">)</span> <span class="c1">; primitives</span>

  <span class="p">(</span><span class="n">C</span> <span class="n">::=</span>
     <span class="p">(</span><span class="nb">+</span> <span class="n">t</span> <span class="k">...</span> <span class="n">C</span> <span class="n">t</span> <span class="k">...</span><span class="p">)</span>
     <span class="p">(</span><span class="n">×</span> <span class="n">t</span> <span class="k">...</span> <span class="n">C</span> <span class="n">t</span> <span class="k">...</span><span class="p">)</span>
     <span class="n">hole</span><span class="p">)</span>
  <span class="p">)</span>

<span class="p">(</span><span class="k">define</span> <span class="n">distribute</span>
  <span class="p">(</span><span class="n">reduction-relation</span>
   <span class="n">Type</span>
   <span class="p">(</span><span class="n">--&gt;</span>
    <span class="p">(</span><span class="n">in-hole</span> <span class="n">C</span> <span class="p">(</span><span class="n">×</span> <span class="p">(</span><span class="nb">+</span> <span class="n">t_a</span> <span class="k">...</span><span class="p">)</span> <span class="n">t_m</span><span class="p">))</span>
    <span class="p">(</span><span class="n">in-hole</span> <span class="n">C</span> <span class="p">(</span><span class="nb">+</span> <span class="p">(</span><span class="n">×</span> <span class="n">t_a</span> <span class="n">t_m</span><span class="p">)</span> <span class="k">...</span><span class="p">)))</span>

   <span class="p">(</span><span class="n">--&gt;</span>
    <span class="p">(</span><span class="n">in-hole</span> <span class="n">C</span> <span class="p">(</span><span class="n">×</span> <span class="n">t_m</span> <span class="p">(</span><span class="nb">+</span> <span class="n">t_a</span> <span class="k">...</span><span class="p">)))</span>
    <span class="p">(</span><span class="n">in-hole</span> <span class="n">C</span> <span class="p">(</span><span class="nb">+</span> <span class="p">(</span><span class="n">×</span> <span class="n">t_a</span> <span class="n">t_m</span><span class="p">)</span> <span class="k">...</span><span class="p">)))</span>
  <span class="p">))</span>

<span class="p">(</span><span class="k">define</span> <span class="p">(</span><span class="nb">flatten</span> <span class="n">term</span><span class="p">)</span>
  <span class="p">(</span><span class="n">apply-reduction-relation*</span> <span class="n">distribute</span> <span class="n">term</span><span class="p">))</span>

<span class="p">(</span><span class="n">test-equal</span>
 <span class="p">(</span><span class="nb">flatten</span> <span class="p">(</span><span class="n">term</span> <span class="p">(</span><span class="n">×</span> <span class="p">(</span><span class="nb">+</span> <span class="n">a</span> <span class="n">b</span><span class="p">)</span> <span class="n">c</span><span class="p">)))</span>
 <span class="o">&#39;</span><span class="p">((</span><span class="ss">+</span> <span class="p">(</span><span class="ss">×</span> <span class="ss">a</span> <span class="ss">c</span><span class="p">)</span> <span class="p">(</span><span class="ss">×</span> <span class="ss">b</span> <span class="ss">c</span><span class="p">))))</span>

<span class="p">(</span><span class="n">test-results</span><span class="p">)</span>
</code></pre></div>



<a name="209204224"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/209204224" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#209204224">(Sep 06 2020 at 01:54)</a>:</h4>
<p>It's been a few years since I've poked at Redex, so if any of y'all have a knack for programming language theory or Racket, I'd love to collab.</p>



<a name="209204355"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/209204355" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#209204355">(Sep 06 2020 at 01:59)</a>:</h4>
<p>If you're interested in modeling transmutability in some other medium, I'm also happy to collaborate! I have a really crisp idea of how everything interacts from working with typic.</p>



<a name="209538071"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/209538071" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#209538071">(Sep 09 2020 at 16:56)</a>:</h4>
<p>Here's a <em>very</em> basic model of transmutability, without references or options:</p>
<div class="codehilite"><pre><span></span><code><span class="kn">#lang </span><span class="nn">racket</span>

<span class="p">(</span><span class="k">require</span> <span class="n">redex</span><span class="p">)</span>

<span class="p">(</span><span class="n">define-language</span>
  <span class="n">layouts</span>

  <span class="p">[</span><span class="n">l</span> <span class="n">::=</span>
     <span class="p">(</span><span class="nb">+</span> <span class="n">l</span> <span class="k">...</span><span class="p">)</span> <span class="c1">; enums</span>
     <span class="p">(</span><span class="n">×</span> <span class="n">l</span> <span class="k">...</span><span class="p">)</span> <span class="c1">; structs</span>
     <span class="n">number</span>    <span class="c1">; exact value</span>
     <span class="n">uninit</span>    <span class="c1">; uninit</span>
     <span class="p">]</span>

  <span class="p">[</span><span class="n">C</span> <span class="n">::=</span>
     <span class="p">(</span><span class="nb">+</span> <span class="n">l</span> <span class="k">...</span> <span class="n">C</span> <span class="n">l</span> <span class="k">...</span><span class="p">)</span>
     <span class="p">(</span><span class="n">×</span> <span class="n">l</span> <span class="k">...</span> <span class="n">C</span> <span class="n">l</span> <span class="k">...</span><span class="p">)</span>
     <span class="n">hole</span><span class="p">]</span>
  <span class="p">)</span>

<span class="p">(</span><span class="k">define</span> <span class="n">distribute</span>
  <span class="p">(</span><span class="n">reduction-relation</span>
   <span class="n">layouts</span>
   <span class="p">[</span><span class="n">--&gt;</span>
    <span class="p">(</span><span class="n">in-hole</span> <span class="n">C</span> <span class="p">(</span><span class="n">×</span> <span class="p">(</span><span class="nb">+</span> <span class="n">l_a</span> <span class="k">...</span><span class="p">)</span> <span class="n">l_m</span><span class="p">))</span>
    <span class="p">(</span><span class="n">in-hole</span> <span class="n">C</span> <span class="p">(</span><span class="nb">+</span> <span class="p">(</span><span class="n">×</span> <span class="n">l_a</span> <span class="n">l_m</span><span class="p">)</span> <span class="k">...</span><span class="p">))]</span>

   <span class="p">[</span><span class="n">--&gt;</span>
    <span class="p">(</span><span class="n">in-hole</span> <span class="n">C</span> <span class="p">(</span><span class="n">×</span> <span class="n">l_m</span> <span class="p">(</span><span class="nb">+</span> <span class="n">l_a</span> <span class="k">...</span><span class="p">)))</span>
    <span class="p">(</span><span class="n">in-hole</span> <span class="n">C</span> <span class="p">(</span><span class="nb">+</span> <span class="p">(</span><span class="n">×</span> <span class="n">l_a</span> <span class="n">l_m</span><span class="p">)</span> <span class="k">...</span><span class="p">))]</span>
  <span class="p">))</span>

<span class="p">(</span><span class="k">define</span> <span class="p">(</span><span class="nb">flatten</span> <span class="n">term</span><span class="p">)</span>
  <span class="p">(</span><span class="nb">car</span> <span class="p">(</span><span class="n">apply-reduction-relation*</span> <span class="n">distribute</span> <span class="n">term</span><span class="p">)))</span>

<span class="p">(</span><span class="n">test-equal</span>
 <span class="p">(</span><span class="nb">flatten</span>
  <span class="o">&#39;</span><span class="p">(</span><span class="ss">×</span> <span class="p">(</span><span class="ss">+</span> <span class="mi">1</span> <span class="mi">2</span><span class="p">)</span> <span class="mi">3</span><span class="p">))</span>
  <span class="o">&#39;</span><span class="p">(</span><span class="ss">+</span> <span class="p">(</span><span class="ss">×</span> <span class="mi">1</span> <span class="mi">3</span><span class="p">)</span> <span class="p">(</span><span class="ss">×</span> <span class="mi">2</span> <span class="mi">3</span><span class="p">)))</span>

<span class="c1">; ---------------------------------------------</span>
<span class="c1">; byte to byte</span>
<span class="p">(</span><span class="n">define-relation</span> <span class="n">layouts</span>
  <span class="n">⥴</span> <span class="n">⊆</span> <span class="n">l</span> <span class="n">×</span> <span class="n">l</span>
  <span class="p">[(</span><span class="n">⥴</span> <span class="n">number</span> <span class="n">number</span><span class="p">)]</span>
  <span class="p">[(</span><span class="n">⥴</span> <span class="n">number</span> <span class="n">uninit</span><span class="p">)]</span>
  <span class="p">[(</span><span class="n">⥴</span> <span class="n">uninit</span> <span class="n">uninit</span><span class="p">)])</span>

<span class="c1">; product to product</span>
<span class="p">(</span><span class="n">define-judgment-form</span> <span class="n">layouts</span>
  <span class="kd">#:mode</span> <span class="p">(</span><span class="n">⥇</span> <span class="n">I</span> <span class="n">I</span><span class="p">)</span>
  <span class="kd">#:contract</span> <span class="p">(</span><span class="n">⥇</span> <span class="p">(</span><span class="n">×</span> <span class="n">l</span> <span class="k">...</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="n">l</span> <span class="k">...</span><span class="p">))</span>

  <span class="p">[(</span><span class="n">⥴</span> <span class="n">l_src</span> <span class="n">l_dst</span><span class="p">)</span> <span class="p">(</span><span class="n">⥇</span> <span class="p">(</span><span class="n">×</span> <span class="n">l_src_n</span> <span class="k">...</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="n">l_dst_n</span> <span class="k">...</span><span class="p">))</span>
   <span class="n">----------------------------------------------------</span> <span class="s2">&quot;nom&quot;</span>
     <span class="p">(</span><span class="n">⥇</span> <span class="p">(</span><span class="n">×</span> <span class="n">l_src</span> <span class="n">l_src_n</span> <span class="k">...</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="n">l_dst</span> <span class="n">l_dst_n</span> <span class="k">...</span><span class="p">))</span>  <span class="p">]</span>


  <span class="c1">; bytes may be truncated from the `dst`; e.g.:</span>
  <span class="c1">; union Transmute { src: u8, dst: () }</span>

  <span class="p">[</span><span class="n">-------------------</span> <span class="s2">&quot;truncate&quot;</span>
   <span class="p">(</span><span class="n">⥇</span> <span class="p">(</span><span class="n">×</span> <span class="n">l</span> <span class="k">...</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span><span class="p">))</span> <span class="p">]</span>


  <span class="c1">; uninit bytes may be conjured from the `src`; e.g.:</span>
  <span class="c1">; union Transmute { src: (), dst: MaybeUninit&lt;u8&gt; }</span>

  <span class="p">[</span><span class="n">------------------------</span> <span class="s2">&quot;barf&quot;</span>
   <span class="p">(</span><span class="n">⥇</span> <span class="p">(</span><span class="n">×</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="n">uninit</span> <span class="k">...</span><span class="p">))</span> <span class="p">]</span>

  <span class="p">)</span>

<span class="c1">; nom</span>
<span class="p">(</span><span class="n">test-judgment-holds</span>
 <span class="p">(</span><span class="n">⥇</span> <span class="p">(</span><span class="n">×</span> <span class="mi">1</span> <span class="mi">2</span> <span class="mi">3</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="mi">1</span> <span class="n">uninit</span> <span class="mi">3</span><span class="p">)))</span>

<span class="c1">; truncate</span>
<span class="p">(</span><span class="n">test-judgment-holds</span>
 <span class="p">(</span><span class="n">⥇</span> <span class="p">(</span><span class="n">×</span> <span class="mi">1</span> <span class="mi">2</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="mi">1</span><span class="p">)))</span>

<span class="c1">; barf uninits</span>
<span class="p">(</span><span class="n">test-judgment-holds</span>
 <span class="p">(</span><span class="n">⥇</span> <span class="p">(</span><span class="n">×</span> <span class="mi">1</span> <span class="n">uninit</span> <span class="n">uninit</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="mi">1</span><span class="p">)))</span>


<span class="c1">; sum to sum</span>
<span class="p">(</span><span class="n">define-judgment-form</span> <span class="n">layouts</span>
  <span class="kd">#:mode</span> <span class="p">(</span><span class="n">⥅</span> <span class="n">I</span> <span class="n">I</span><span class="p">)</span>
  <span class="kd">#:contract</span> <span class="p">(</span><span class="n">⥅</span> <span class="p">(</span><span class="nb">+</span> <span class="n">l</span> <span class="k">...</span><span class="p">)</span> <span class="p">(</span><span class="nb">+</span> <span class="n">l</span> <span class="k">...</span><span class="p">))</span>

  <span class="c1">; there must exist some variant of the dst such that</span>
  <span class="c1">; every variant of the src ⥇ that variant of the dst</span>
  <span class="p">[</span>              <span class="p">(</span><span class="n">⥇</span> <span class="n">l_src</span> <span class="n">l_dst</span><span class="p">)</span> <span class="k">...</span>
   <span class="n">-----------------------------------------</span> <span class="s2">&quot;∀src.∃dst.src⥇dst&quot;</span>
   <span class="p">(</span><span class="n">⥅</span> <span class="p">(</span><span class="nb">+</span> <span class="n">l_src</span> <span class="k">...</span><span class="p">)</span> <span class="p">(</span><span class="nb">+</span> <span class="k">_</span> <span class="k">...</span> <span class="n">l_dst</span> <span class="k">_</span> <span class="k">...</span><span class="p">))</span> <span class="p">]</span>
  <span class="p">)</span>

<span class="p">(</span><span class="n">test-judgment-holds</span>
 <span class="p">(</span><span class="n">⥅</span> <span class="p">(</span><span class="nb">+</span> <span class="p">(</span><span class="n">×</span> <span class="mi">1</span><span class="p">))</span> <span class="p">(</span><span class="nb">+</span> <span class="p">(</span><span class="n">×</span> <span class="mi">1</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="mi">2</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="mi">3</span><span class="p">))))</span>

<span class="p">(</span><span class="n">test-judgment-holds</span>
 <span class="p">(</span><span class="n">⥅</span> <span class="p">(</span><span class="nb">+</span> <span class="p">(</span><span class="n">×</span> <span class="mi">2</span><span class="p">))</span> <span class="p">(</span><span class="nb">+</span> <span class="p">(</span><span class="n">×</span> <span class="mi">1</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="mi">2</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="mi">3</span><span class="p">))))</span>


<span class="p">(</span><span class="n">test-judgment-holds</span>
 <span class="p">(</span><span class="n">⥅</span> <span class="p">(</span><span class="nb">+</span> <span class="p">(</span><span class="n">×</span> <span class="mi">3</span><span class="p">))</span> <span class="p">(</span><span class="nb">+</span> <span class="p">(</span><span class="n">×</span> <span class="mi">1</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="mi">2</span><span class="p">)</span> <span class="p">(</span><span class="n">×</span> <span class="mi">3</span><span class="p">))))</span>

<span class="p">(</span><span class="n">test-results</span><span class="p">)</span>

<span class="c1">; is transmutable</span>
<span class="p">(</span><span class="k">define</span> <span class="p">(</span><span class="n">transmutable</span> <span class="n">src</span> <span class="n">dst</span><span class="p">)</span>
  <span class="p">(</span><span class="n">term-let</span> <span class="p">([</span><span class="n">src</span> <span class="p">(</span><span class="nb">flatten</span> <span class="n">src</span><span class="p">)]</span>
             <span class="p">[</span><span class="n">dst</span> <span class="p">(</span><span class="nb">flatten</span> <span class="n">dst</span><span class="p">)])</span>
    <span class="p">(</span><span class="n">traces</span> <span class="n">⥅</span> <span class="p">(</span><span class="n">⥅</span> <span class="n">src</span> <span class="n">dst</span><span class="p">))))</span>
</code></pre></div>



<a name="209538438"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/209538438" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#209538438">(Sep 09 2020 at 17:00)</a>:</h4>
<p>I don't yet have a great sense for when to reach for a <code>reduction-relation</code>, <code>define-metafunction</code>, <code>define-relation</code> or <code>define-judgment-form</code>.  In some contexts, they're interchangeable. The syntax of <code>define-judgment-form</code> felt the most natural, but all of Redex's cool GUI stuff is focused on reduction-relations.</p>



<a name="209538836"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/209538836" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#209538836">(Sep 09 2020 at 17:02)</a>:</h4>
<p>This model is a little unrealistic as an implementation guide since it encodes <code>u8</code> as an enum of 256 variants. <span aria-label="sweat smile" class="emoji emoji-1f605" role="img" title="sweat smile">:sweat_smile:</span></p>



<a name="210327288"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/210327288" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#210327288">(Sep 16 2020 at 22:19)</a>:</h4>
<p>I've made a <a href="https://github.com/jswrenn/safer-transmutation-redex">Github repo</a> for the Redex model.</p>



<a name="210327422"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/210327422" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#210327422">(Sep 16 2020 at 22:21)</a>:</h4>
<p>It's still <em>very</em> incomplete, and I would love some help to flesh it out.</p>



<a name="210328706"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/210328706" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#210328706">(Sep 16 2020 at 22:37)</a>:</h4>
<p>There are three challenges:</p>
<ul>
<li>the layout grammar is too primitive to efficiently cover some useful cases</li>
<li>the <code>~</code> judgment form doesn't include all necessary algebraic transformations of types</li>
<li>the <code>→</code> judgment form doesn't model all combinations of types</li>
</ul>



<a name="210471353"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/210471353" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#210471353">(Sep 18 2020 at 01:43)</a>:</h4>
<p><span aria-label="scissors" class="emoji emoji-2702" role="img" title="scissors">:scissors:</span><br>
<a href="/user_uploads/4715/8l2kcticI1OzrGmbwCL8XmIs/screenshot-github.com-2020.09.17-21_31_18.png">screenshot-github.com-2020.09.17-21_31_18.png</a></p>
<div class="message_inline_image"><a href="/user_uploads/4715/8l2kcticI1OzrGmbwCL8XmIs/screenshot-github.com-2020.09.17-21_31_18.png" title="screenshot-github.com-2020.09.17-21_31_18.png"><img src="/user_uploads/4715/8l2kcticI1OzrGmbwCL8XmIs/screenshot-github.com-2020.09.17-21_31_18.png"></a></div>



<a name="210471540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/210471540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#210471540">(Sep 18 2020 at 01:47)</a>:</h4>
<p>In Redex, it's really easy to mix up non-terminal names in the language grammar with the names of metafunctions/judgments/etc. So, <em>clearly</em>, the appropriate response is to adopt a naming convention that clearly distinguishes between the two: alphanumerics for terms, and mathematical operators for metafunctions.</p>
<p>I have a metafunction which snips bytes.</p>
<p><code>✂</code> is <em>definitely</em> a mathematical operator. ;-)</p>



<a name="211160546"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/211160546" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#211160546">(Sep 24 2020 at 17:02)</a>:</h4>
<p>I've translated the redex model to Rust: <a href="https://play.rust-lang.org/?version=nightly&amp;mode=debug&amp;edition=2018&amp;gist=a65d762ff317feda046a107c542ce44c">https://play.rust-lang.org/?version=nightly&amp;mode=debug&amp;edition=2018&amp;gist=a65d762ff317feda046a107c542ce44c</a></p>



<a name="211160721"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/211160721" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#211160721">(Sep 24 2020 at 17:04)</a>:</h4>
<p>With Redex, I was struggling to do the manual bookkeeping of making sure I had exhaustively accounted for every combination of layout types. With Rust, it's easy: <code>match</code> requires exhaustivity! <span aria-label="grinning" class="emoji emoji-1f600" role="img" title="grinning">:grinning:</span></p>



<a name="211161430"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/211161430" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#211161430">(Sep 24 2020 at 17:10)</a>:</h4>
<p>It's not a complete model, and it's not even a complete minimal model. It's <em>mostly</em> complete. There are two <code>todo!()</code>s relating to basically the same task...</p>
<p>A "bytes" is a tuple indicating its non-zero length and validity. The validity is either <code>Uninitialized</code> or <code>Initialized { min, max }</code>, where <code>min..max</code> encodes the valid instantiations of its bits.</p>
<p>The <code>split_bytes_at</code> function takes a <code>Bytes</code> of some length <code>l</code> and an index <code>n</code>, and produces a new layout sequence consisting of bytes of length <code>n</code> and bytes of length <code>l - n</code> — adjusting their validity as necessary.</p>
<p>For <code>Bytes</code> whose validity is <code>Uninitialized</code>, this is easy: you end up with a sequence of two <code>Uninitialized</code> bytes.</p>
<p>For <code>Bytes</code> whose validity is <code>Initialized</code>, this isn't easy, and the result depends on endian. Figuring this out is the <code>todo</code>.</p>



<a name="211162897"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/211162897" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#211162897">(Sep 24 2020 at 17:22)</a>:</h4>
<p>For instance, a <code>NonZeroU16</code> is represented as:</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="w">  </span><span class="n">Bytes</span><span class="p">(</span><span class="mi">2</span><span class="p">,</span><span class="w"> </span><span class="n">Initialized</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">min</span>: <span class="mi">1</span><span class="p">,</span><span class="w"> </span><span class="n">max</span>: <span class="kt">u16</span>::<span class="n">MAX</span><span class="w"> </span><span class="p">})</span><span class="w"></span>
</code></pre></div>

<p>Calling <code>.split_bytes_at(1)</code> should produce (abbreviated slightly to elide newtypes and boxes):</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="cm">/* sum encodes a choice between two layouts */</span><span class="w"></span>
<span class="n">Sum</span><span class="p">(</span><span class="w"></span>
<span class="w">  </span><span class="cm">/* prod encodes a sequence of two layouts */</span><span class="w"></span>
<span class="w">  </span><span class="cm">/* either the first byte may be zero */</span><span class="w"></span>
<span class="w">  </span><span class="n">Prod</span><span class="p">(</span><span class="w"></span>
<span class="w">    </span><span class="n">Bytes</span><span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="w"> </span><span class="n">Initialized</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">min</span>: <span class="mi">0</span><span class="p">,</span><span class="w"> </span><span class="n">max</span>: <span class="kt">u8</span>::<span class="n">MAX</span><span class="w"> </span><span class="p">}),</span><span class="w"></span>
<span class="w">    </span><span class="n">Bytes</span><span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="w"> </span><span class="n">Initialized</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">min</span>: <span class="mi">1</span><span class="p">,</span><span class="w"> </span><span class="n">max</span>: <span class="kt">u8</span>::<span class="n">MAX</span><span class="w"> </span><span class="p">})),</span><span class="w"></span>
<span class="w">  </span><span class="cm">/* or the second byte may be zero */</span><span class="w"></span>
<span class="w">  </span><span class="n">Prod</span><span class="p">(</span><span class="w"></span>
<span class="w">    </span><span class="n">Bytes</span><span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="w"> </span><span class="n">Initialized</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">min</span>: <span class="mi">1</span><span class="p">,</span><span class="w"> </span><span class="n">max</span>: <span class="kt">u8</span>::<span class="n">MAX</span><span class="w"> </span><span class="p">}),</span><span class="w"></span>
<span class="w">    </span><span class="n">Bytes</span><span class="p">(</span><span class="mi">1</span><span class="p">,</span><span class="w"> </span><span class="n">Initialized</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">min</span>: <span class="mi">0</span><span class="p">,</span><span class="w"> </span><span class="n">max</span>: <span class="kt">u8</span>::<span class="n">MAX</span><span class="w"> </span><span class="p">})))</span><span class="w"></span>
</code></pre></div>



<a name="211165538"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/211165538" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#211165538">(Sep 24 2020 at 17:42)</a>:</h4>
<p><strong>What's the general algorithm that describes this?</strong></p>



<a name="211827424"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/211827424" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#211827424">(Sep 30 2020 at 21:08)</a>:</h4>
<p><a href="https://github.com/jswrenn/safer-transmutation-redex/commit/561b664e029ea046d6033e21a19630ca9a18f24b#diff-851df0bc02a9b59fb1b178a14ae4e52d">I think we worked out an algorithm for this in the little-endian case</a>, but I decided to simplify the model by nixing the <code>Bytes</code> layout variant for a <code>Byte</code> layout variant (which always encodes <em>one</em> byte).</p>



<a name="211827860"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/216762-project-safe-transmute/topic/Modeling%20Transmutability/near/211827860" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Wrenn <a href="https://rust-lang.github.io/zulip_archive/stream/216762-project-safe-transmute/topic/Modeling.20Transmutability.html#211827860">(Sep 30 2020 at 21:12)</a>:</h4>
<p>The obstacle I'm facing now is handling transmutations into sums (aka unions).</p>
<p>Concretely, this:</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="n">Atom</span><span class="p">(</span><span class="n">Byte</span><span class="p">(</span><span class="n">Init</span><span class="p">(</span><span class="mi">0</span><span class="o">..=</span><span class="mi">127</span><span class="p">)))</span><span class="w"></span>
</code></pre></div>

<p><em>should</em> be transmutable into this:</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="n">Sum</span><span class="p">(</span><span class="k">box</span><span class="w"> </span><span class="n">Atom</span><span class="p">(</span><span class="n">Byte</span><span class="p">(</span><span class="n">Init</span><span class="p">(</span><span class="mi">0</span><span class="o">..=</span><span class="mi">126</span><span class="p">))),</span><span class="w"></span>
<span class="w">    </span><span class="k">box</span><span class="w"> </span><span class="n">Atom</span><span class="p">(</span><span class="n">Byte</span><span class="p">(</span><span class="n">Init</span><span class="p">(</span><span class="mi">127</span><span class="o">..=</span><span class="mi">255</span><span class="p">)))),</span><span class="w"></span>
</code></pre></div>

<p>It's an easy-enough requirement to state as prose: the src layout must be covered by one or more of the alternatives in the dst layout.</p>
<p>Mechanically, though, I don't really know how to implement this, and would love some help!</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>